/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free oftware Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.io.PrintStream;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;

import alloy.ast.ASTDepthFirstReturnVisitor;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.BinaryFormula;
import alloy.ast.BinaryIntExpr;
import alloy.ast.CardinalityExpr;
import alloy.ast.CompOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.DeclIter;
import alloy.ast.ElemFormula;
import alloy.ast.ElemIntFormula;
import alloy.ast.EmptyFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.GenericConstExpr;
import alloy.ast.IdentityExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IfThenElseIntExpr;
import alloy.ast.ImplicationFormula;
import alloy.ast.IntCompOp;
import alloy.ast.IntExpr;
import alloy.ast.IntExprOp;
import alloy.ast.Leaf;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.LiteralIntExpr;
import alloy.ast.LogicOp;
import alloy.ast.MultiplicityExpr;
import alloy.ast.NegFormula;
import alloy.ast.Node;
import alloy.ast.Op;
import alloy.ast.QuantifiedExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.SigExpr;
import alloy.ast.SumExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.ast.UniversalExpr;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.bool.BoolSwitch;
import alloy.bool.BooleanFormula;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.MultiDimArray;
import alloy.util.MultiDimIter;
import alloy.util.Params;

/**
 * Translates {@link alloy.ast.Node}s into a {@link BooleanFormulaSAT}
 * representation. Boolean variables are allocated to each relation; for each
 * {@link alloy.ast.Node}, we then generate one or more {@link BooleanFormula}
 * s which together evaluate to the correct value of the AST node for given
 * values of the Boolean variables allocated to the state.
 * <p>
 * The {@link #visit}methods return a {@link Transl}of the corresponding
 * {@link Node}.
 * <p>
 * {@link TranslVisitor}also gathers some summary information about the formula
 * being translated. This includes the list of relations (leaves to which groups
 * of Boolean variables were allocated), and a list of {@link BasicType}s used
 * in the formula. This information is used for a number of purposes after
 * translation is finished -- e.g. for
 * {@link alloy.symm.SymmetryBreaker symmetry breaking},
 * {@link alloy.sharbool template detection}, and for displaying the results.
 * <p>
 * <em>Note</em>: translation of relations (i.e. {@link ExprTranl}s produced
 * from {@link LeafExpr leaves}currently must use only Boolean constants or
 * Boolean variables -- no general Boolean formulas. I.e. to each tuple of a
 * relation, we must allocate either a Boolean variable or a Boolean constant.
 * This is so we can identify the variable allocated to each tuple, and let the
 * user edit an instance. Code that depends on this restriction: look for uses
 * of {@link BooleanFormula#isConst},{@link BooleanFormula#isLiteral}and
 * {@link BooleanFormula#getLiteral}-- currently in
 * {@link alloy.gui.RelationEditor}.
 * <p>
 * The nodes that need to be translated are listed below; other have been
 * desugared in prior passes.
 * <p>
 * Formulas -------------- FormulaSeq, Formulas - implicitly conjoined formulas.
 * note that these may be empty and may contain other FormulaSeqs. BinaryFormula -
 * formula (and | or | iff) formula ElemFormula - formula (in | = | :) formula
 * ElemIntFormula - intexpr ( = | < | = < | > | >=) intexpr EmptyFormula - this
 * is just a placeholder, nothing needs to be done. used in the else clause of
 * implication formulas with no else, for example ImplicationFormula - formula
 * then formula (else formula) NegFormula - not formula QuantifiedExpr -
 * quantifier expr QuantifiedFormula - quantifier decls | formula. For
 * quantified variables, you should just have to look at the type of the
 * multiplicity expression in the decl to figure out the scope, but everything
 * else should be explicit. For example:
 * 
 * sig A {}
 * all x: A | F(x)
 * 
 * the formula will desugar to
 * 
 * all x: A | x in A and # x = 1 => F(x)
 * 
 * Hopefully this will be a good representation for translation.
 * 
 * Expressions (starred expressions are leaves) ------------------
 * BinaryExpr - expr (. | + | - | & | -> | ++) expr. Note that the JOIN_DOT,
 * JOIN_DOUBLECOLON, and JOIN_BRACKETS operators are all equivalent at this
 * point (no worries about precedence). ComprehensionExpr - { decls | formula }.
 * The notes for desugaring QuantifiedFormulas above also apply here, except the
 * desugaring is { x: A | F(x) } to { x: A | x in A and # x = 1 and F(x) }
 * 
 * EmptyExpr - similar function to EmptyFormula EmptySetExpr, IdentityExpr,
 * UniversalExpr - the none, iden, and univ constructs. (*) IntExprCastExpr -
 * Int intexpr SigExpr - explained in previous email (*) UnaryExpr - (^ | * | ~)
 * expr VariableExpr - either a quantified variable or a field name on the right
 * side of a join (distinguish using leaf id) (*)
 * 
 * Int Expressions (starred expressions are leaves) -----------------------
 * BinaryIntExpr - intexpr (+ | -) intexpr CardinalityExpr - # expr
 * ExprCastIntExpr - int expr (expr has type Int) LiteralIntExpr - number (*)
 * SumExpr - sum expr SumIntExpr - sum decls | intexpr. NOTE: the constraints of
 * these declarations are not desugared because i did not know how to do it in a
 * source-to-source transformation (see previous email). You may have to deal
 * with them directly if we can't think of anything.
 */
public class TranslVisitor extends ASTDepthFirstReturnVisitor implements TranslInfo {
    /**
	 * {@link Map}from a {@link LeafId}to its {@link Transl}ation: array of
	 * Boolean variables or switchable constants allocated to this leaf. (Note
	 * that all {@link Leaf}s are currently {@link Expr}s). When processing a
	 * leaf with a given {@link LeafId}for the first time, we create a
	 * translation of the leaf, allocating new Boolean variables. Thereafter, we
	 * retrieve this translation when we hit another instance of the same leaf
	 * (as related by {@link LeafId}).
	 */
    private Map /* LeafId->Transl */ _leafTransl = new TreeMap();

    /**
     * Map from LeafId of a quantified variable to the {@link QVarIterationInfo}
     * object which gives the values over which the variable iterates.
     */
    private Map /* LeafId->QVarIterationInfo */ _qvarIterInfo = new TreeMap();

    /**
	 * {@link Transl}ation of each node; used for displaying the values of all
	 * internal nodes for a given assignment of Boolean variables. This can help
	 * understand why a particular instance of a model does not satisfy the
	 * specified constraints, and which constraints exactly does it break. This
	 * map is built during translation, but is not used in translation -- the
	 * {@link TranslVisitor}can be asked for this map once translation is
	 * finished.
	 */
    private Map _node2transl = new TreeMap();

    /**
	 * relations: what to display once we find a solution. These are exactly
	 * those leaves for which we decided to allocate new Boolean variables.
	 * {@link Map}from {@link LeafId}to {@link LeafExpr}. Note that the
	 * {@link LeafExpr}is just the first mention of this relation that we
	 * encounter in the AST -- there may be other {@link LeafExpr}s in the AST
	 * referring to the same relation (having the same {@link LeafId}).
	 */
    private Map _relations = new TreeMap();

    /**
	 * For each quantified variable, the {@link BoolSwitch}that will be used
	 * for holding the current value of the variable during tree traversals.
	 * {@link Map}from {@link LeafId}of the {@link VariableExpr}to a
	 * {@link BoolSwitch}.
	 */
    // eclipse says this is never used
    //private Map _var2switch = new TreeMap();

    /** Allocator of Boolean variables. */
    private BoolVarAllocator _boolVarAllocator;

    /**
     * Allocator of Boolean variables to relation.
     */
    private RelationAllocator _relationAllocator;

    /**
	 * The {@link Formula}we translated (the root of it). Stored here in order
	 * to have all the information about the formula in one place.
	 */
    // eclipse says this is never read
    //private Formula _formula;

    /**
     * {@link ASTInfoVisitor} holding some summary info about the AST.
     */
    private ASTInfoVisitor _astInfoVisitor;

    /**
	 * Number of {@link BooleanFormula}nodes allocated. If this number exceeds
	 * the value of the global parameter MAIN.maxBoolNodes, translation aborts.
	 * This is done to ensure that if there are not enough resources to do the
	 * translation, we exit gracefully rather than crash with an out-of-memory
	 * error.
	 */
    private long _boolNodesAllocated = 0;

      /////////////
     // Methods //
    /////////////

    /** Utility routine to save the translation of the node, and return the translation. */
    private Transl _saveTransl(Node node_, Transl transl_) {
//  System.out.println("translation of " + node_.nodeString() +
//             " is " + transl_);
    //System.out.println("saving: " + node_.nodeString());
    Dbg.chk(node_); Dbg.chk(transl_);
    _node2transl.put(node_, transl_);
    int nodeId = getNodeID(node_);
    for (Iterator boolFormIter = transl_.getBooleanFormulas().iterator(); boolFormIter.hasNext();) {
        BooleanFormula bf = (BooleanFormula)boolFormIter.next();
        bf.setNodeSrc(nodeId);
    }
    return transl_;
    }

    /**
	 * Count a {@link BooleanFormula}node allocation. If we have exceeded the
	 * limit specified by the global parameter MAIN.maxBoolNodes, abort the
	 * translation.
	 */
    private void _countBoolNode() throws TranslException {
    if (_boolNodesAllocated++ > Params.glob.getLongParam("MAIN", "maxBoolNodes"))
        throw new TranslException("Too many Boolean nodes.  \nCheck for higher-order quantifiers.\n" +
                      "Try increasing MAIN.maxBoolNodes parameter");
    if (Runtime.getRuntime().freeMemory() < 100000) {
        System.gc(); System.gc(); System.gc();
        if (Runtime.getRuntime().freeMemory() < 100000)
        throw new TranslException("Translation ran out of memory.");
    }
    }

    private TranslVisitor(RelationAllocator relationAlloc_) {
    _relationAllocator = relationAlloc_;
    _boolVarAllocator = relationAlloc_.getBoolVarAllocator();
    }

    /**
     * Translate the given Alloy {@link Formula} (in translatable AST form)
     * to a Boolean formula.
     *
     * @param f_ Alloy formula, in translatable AST form, to be translated
     * @param relationAlloc_ allocator of Boolean variables to relations
     * @throws TranslException if the formula cannot be translated due to some
     *                         limitations of the translator implementation or
     *                         due to lack of resources e.g. memory
     */
    public static TranslInfo translate(Formula f_,
                       ASTInfoVisitor astInfoVisitor_,
                       RelationAllocator relationAlloc_)
    throws TranslException {
    f_.applyVisitor(new TranslatableASTCheckVisitor());
    TranslVisitor translator = new TranslVisitor(relationAlloc_);
    translator._setFormula(f_);
    translator._astInfoVisitor = astInfoVisitor_;
    f_.applyReturnVisitor(translator);
    return translator;
    }

    /**************/
    /*** Leaves ***/
    /**************/

    /** Translate {@link Expr}-valued leaf nodes (relations). */
    private Object _visitLeafExpr(LeafExpr leafExpr_) {
	    Dbg.chk(leafExpr_.getLeafId());
	    /* See if we've already translated this relation.
	       If yes, then we have already allocated the correct array
	       of Boolean variables; just return the same array. */
	    ExprTransl result = (ExprTransl)_leafTransl.get(leafExpr_.getLeafId());
	    if (result != null) return _saveTransl(leafExpr_, result);
	
	    /* Allocate fresh Boolean variables to the elements of the array.
	       From each Boolean variable, construct a Boolean formula
	       consisting of that one variable, and put it into the array. */
	    result = _relationAllocator.getRelationTransl(leafExpr_.getLeafId());
	
	    /* Cache the result, so that when we encounter another reference
	       to the same relation, we do not allocate another set
	       of Boolean variables to it. */
	    _leafTransl.put(leafExpr_.getLeafId(), result);
	    _relations.put(leafExpr_.getLeafId(), leafExpr_);
	
	    return _saveTransl(leafExpr_, result);
    }  // _visitLeafExpr()

    /**
	 * Print out the value of each relation for the given instance. (We gathered
	 * a list of relations, {@link #_relations}, during translation.)
	 * 
	 * Specify output stream by 2nd argument, or standard output by default.
	 */
    public void interpretRelations(boolean[] assignment_) {
        interpretRelations(assignment_, System.out);
    }

    /**
	 * Print the value of the given instance (i.e. the values of all relations)
	 * to the given stream. Used e.g. by the
	 * {@link alloy.cli.AlloyCLI command-line interface} to output the results
	 * of analysis.
	 */
    public void interpretRelations(boolean[] assignment_, PrintStream ps) {
        ps.println("=============================================================");

		//
		// Print the integer value associated with each atom of the special basic type Int,
		// if it was used in the model.
		//
		BasicType intType = getIntType();
		if (intType != null) {
		    // determine the LeafId corresponding to the Int set
		    LeafId intLeafId = null;
		    for (Iterator relIter = _astInfoVisitor.getRelations().iterator(); intLeafId == null && relIter.hasNext();) {
			LeafId leafId = (LeafId)relIter.next();
			RelationType relType = _astInfoVisitor.getLeafType(leafId);
			if (relType.numBasicTypes() == 1 &&
			    relType.getBasicTypeAt(0) == intType)
			    intLeafId = leafId;
		    }
		    Dbg.chk(intLeafId);
		    ExprTransl intTransl = (ExprTransl)_leafTransl.get(intLeafId);
		    Dbg.chk(intTransl!=null && intTransl.getType().numBasicTypes() == 1 &&
			    intTransl.getType().getBasicTypeAt(0) == intType);
		    
		    ps.println("Integers:");
		    for (int intAtom=0; intAtom<intType.getScope(); intAtom++) {
			if (intTransl.getTupleFormula(intAtom).interpret(assignment_)) {
			    IntTransl it = _relationAllocator.getIntAtomTransl(intAtom);
			    ps.println("Int_" + intAtom + " = " +
				       it.interpretAsInt(assignment_));
			}
		    }
		    ps.println();
		}

		// Print the value of each relation.
		for (Iterator entryIter = _relations.entrySet().iterator(); entryIter.hasNext();) {
		    Map.Entry entry = (Map.Entry)entryIter.next();
		    LeafId leafId = (LeafId)entry.getKey();
		    LeafExpr leafExpr = (LeafExpr)entry.getValue();
		    String name = leafExpr.nodeString();
		    ExprTransl transl = (ExprTransl)_leafTransl.get(leafId);
		    RelationType relType = leafExpr.getType().toRelationType();
		    String firstTypeName = relType.getBasicTypeAt(0).toShortString();
		    name = (relType.numBasicTypes() == 1) ?
			name : 
			firstTypeName + "$" + name;
		    ps.println("---------------------------");
		    ps.println("relation: " + name + " (type: " + relType.toShortString() + ")");
		    ps.println(transl.interpret(assignment_));
		}
		ps.println("=============================================================");
    }  // interpretRelations()

    /** Translate as a relation */
    public Object visit(SigExpr sigExpr_) { return _visitLeafExpr((LeafExpr)sigExpr_); }

    /**
	 * If this refers to a field, translate as a relation; otherwise, allocate
	 * an {@link ExprTransl}of switchable constants.
	 */
    public Object visit(VariableExpr variableExpr_) {
	    ExprTransl result = (ExprTransl)_leafTransl.get(variableExpr_.getLeafId());
	    if (result != null) return _saveTransl(variableExpr_, result);
	
	    return variableExpr_.isQuantified ?
	            _visitQuantifiedVariable(variableExpr_, variableExpr_.getType().toRelationType(),  variableExpr_.getLeafId()) :
	                _visitLeafExpr((LeafExpr)variableExpr_);
    }

    private MultiDimArray _allocFormulas(RelationType relType_) {
        //Dbg.info(relType_.toString());
	    int[] dims = new int[relType_.numBasicTypes()];
	    for (int i=0; i<dims.length; i++)
	        dims[i] = relType_.getBasicTypeAt(i).getScope();
	    return new MultiDimArray(dims);
    }

    private Object _visitQuantifiedVariable(VariableExpr varExpr_,
                        RelationType relType_,
                        LeafId leafId_) {
	    QVarIterationInfo iterInfo =
	        (QVarIterationInfo)_qvarIterInfo.get(leafId_);
	    ExprTransl result = iterInfo.getQVarTransl();
	    _leafTransl.put(leafId_, result);
	    return _saveTransl(varExpr_, result);
    }

    /****************/
    /*** Formulas ***/
    /****************/

    public Object visit(ElemFormula elemFormula_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(elemFormula_));
	    ExprTransl leftTransl = (ExprTransl)elemFormula_.getLeft().applyReturnVisitor(this);
	    ExprTransl rightTransl = (ExprTransl)elemFormula_.getRight().applyReturnVisitor(this);
	    FormulaTransl result = null;
	    CompOp op = elemFormula_.getOp();
	    if (op.isNegated()) op = op.negation();
	    
	    if (op.equals(CompOp.SUBSETCOLON) || op.equals(CompOp.SUBSETIN)) {
	        result = leftTransl.subset(rightTransl);
	    } else if (op.equals(CompOp.EQUALS)) {
	        result = leftTransl.equality(rightTransl);
	    } else {
	        Dbg.fail("no such comp op");
	    }
	    
	    if (elemFormula_.getOp().isNegated()) result = result.not();
	    return _saveTransl(elemFormula_, result);
    }

    /** Implicitly conjoined {@link alloy.ast.Formula}s. */
    public Object visit(FormulaSeq formulaSeq_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(formulaSeq_));
	    List formulas = new ArrayList();
	    for (Iterator formulaIter = formulaSeq_.getFormulas().getFormulaIter();
	         formulaIter.hasNext();) {
	        Formula formula = (Formula)formulaIter.next();
	        FormulaTransl formulaTransl = (FormulaTransl)formula.applyReturnVisitor(this);
	        formulas.add(formulaTransl.formula);
	    }
	    _countBoolNode();
	    FormulaTransl result = new FormulaTransl(BooleanFormula.makeAnd(formulas));
	    _saveTransl(formulaSeq_.getFormulas(), result);
	    return _saveTransl(formulaSeq_, result);
    }

    public Object visit(Node node_) { Dbg.fatal("untranslated node: " + node_); return null; }

    /** Treat as constant TRUE. */
    public Object visit(EmptyFormula emptyFormula_) { return _saveTransl(emptyFormula_, FormulaTransl.TRUE()); }

    public Object visit(BinaryFormula binaryFormula_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(binaryFormula_));
	    FormulaTransl leftTransl = (FormulaTransl)binaryFormula_.getLeft().applyReturnVisitor(this);
	    FormulaTransl rightTransl = (FormulaTransl)binaryFormula_.getRight().applyReturnVisitor(this);
	    Transl result = null;
	    
	    LogicOp op = binaryFormula_.getOp();
	    if (op.equals(LogicOp.AND)) {
	        result = leftTransl.and(rightTransl);
	    } else if (op.equals(LogicOp.OR)) {
	        result = leftTransl.or(rightTransl);
	    } else if (op.equals(LogicOp.IFF)) {
	        result = leftTransl.iff(rightTransl);
	    } else {
	        Dbg.fail("no such logic op");
	    }
	    
	    return _saveTransl(binaryFormula_, result);
    }

    public Object visit(ImplicationFormula implFormula_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(implFormula_));
	    FormulaTransl ifTransl = (FormulaTransl)implFormula_.getIfFormula().applyReturnVisitor(this);
	    FormulaTransl thenTransl = (FormulaTransl)implFormula_.getThenFormula().applyReturnVisitor(this);
	    FormulaTransl elseTransl = (FormulaTransl)implFormula_.getElseFormula().applyReturnVisitor(this);
	    return _saveTransl(implFormula_, ifTransl.implies(thenTransl).and(ifTransl.not().implies(elseTransl)));
    }

    public Object visit(NegFormula negFormula_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(negFormula_));
	    FormulaTransl formulaTransl = (FormulaTransl)negFormula_.getFormula().applyReturnVisitor(this);
	    return _saveTransl(negFormula_, formulaTransl.not());
    }

    public Object visit(QuantifiedExpr quantExpr_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(quantExpr_));
	
	    ExprTransl exprTransl = (ExprTransl)quantExpr_.getExpr().applyReturnVisitor(this);
	
	    FormulaTransl result = null;
	    Quantifier quant = quantExpr_.getQuantifier();
	    
	    if (quant.equals(Quantifier.LONE))
	        // more compact translation than cardinality.le(IntTransl.ONE)
	        result = exprTransl.sole();
	    else {
	        IntTransl cardinality = IntTransl.fromExprTransl(exprTransl);
	        if (quant.equals(Quantifier.NO)){
	            result = cardinality.eq(IntTransl.ZERO);
	        } else if (quant.equals(Quantifier.ONE)) {
	            result = cardinality.eq(IntTransl.ONE);
	        } else if (quant.equals(Quantifier.SOME)) {
	            result = cardinality.gt(IntTransl.ZERO);
	        } else if (quant.equals(Quantifier.ALL)) {
	            Dbg.unimpl("all expr");
	        }
	    }
	    return _saveTransl(quantExpr_, result);
    }

    public Object visit(SumIntExpr sumIntExpr_) {
    BooleanFormula.setDefaultNodeSrc(getNodeID(sumIntExpr_));

    for (DeclIter declIter = new DeclIter(sumIntExpr_); declIter.hasNext();) {
        declIter.next();
        LeafId leafId = declIter.getLeafId();
        _qvarIterInfo.put(leafId, QVarValGenerator.constructQVarIterationInfo(leafId, _astInfoVisitor));
    }

    IntTransl bodyTransl = (IntTransl)sumIntExpr_.getBody().applyReturnVisitor(this);
    BooleanFormula[] result = bodyTransl.getBits();

    for (DeclIter declIter = new DeclIter(sumIntExpr_); declIter.hasNext();) {
        Variable var = declIter.nextVar();
        LeafId leafId = declIter.getLeafId();
        QVarIterationInfo iterInfo = (QVarIterationInfo)_qvarIterInfo.get(leafId);
        BoolSwitch boolSwitch = iterInfo.getBoolSwitch();
        long[] boolSwitchValues = iterInfo.getBoolSwitchValues();

        List /* of IntTransl */ intTransls = new ArrayList();

        for (int switchValNum=0; switchValNum<boolSwitchValues.length; switchValNum++) {
        BooleanFormula[] instance = new BooleanFormula[result.length];
        for (int i=0; i<instance.length; i++) {
            _countBoolNode();
            instance[i] = BooleanFormula.makeSwitch(boolSwitch, boolSwitchValues[switchValNum], result[i]);
        }
        intTransls.add(new IntTransl(instance));
        }

        result = IntTransl.makeSum(intTransls).getBits();
    }
    return _saveTransl(sumIntExpr_, new IntTransl(result));
    }  // visit(sumIntExpr_)

    public Object visit(QuantifiedFormula quantForm_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(quantForm_));
	
	    //System.out.println("*****************************");
	    //System.out.println("NOW TRANSLATING: " + quantForm_.nodeString());
	
	    for (DeclIter declIter = new DeclIter(quantForm_); declIter.hasNext();) {
	        declIter.next();
	        LeafId leafId = declIter.getLeafId();
	
		//System.out.println("VARIABLE " + declIter.getVariable() + " id " + leafId);
	
	        _qvarIterInfo.put(leafId, QVarValGenerator.constructQVarIterationInfo(leafId, _astInfoVisitor));
	    }
	
	    FormulaTransl formulaTransl =
	        (FormulaTransl)quantForm_.getFormula().applyReturnVisitor(this);
	
	    BooleanFormula result = formulaTransl.formula;
	    Quantifier quant = quantForm_.getQuantifier();
	    Dbg.chk(quant.equals(Quantifier.ALL) || quant.equals(Quantifier.SOME));
	    for (DeclIter declIter = new DeclIter(quantForm_); declIter.hasNext();) {
	        Variable var = declIter.nextVar();
	        String varName = var.nodeString();
	        LeafId leafId = declIter.getLeafId();
	        QVarIterationInfo iterInfo = (QVarIterationInfo)_qvarIterInfo.get(leafId);
	        BoolSwitch boolSwitch = iterInfo.getBoolSwitch();
	        long[] boolSwitchValues = iterInfo.getBoolSwitchValues();
	        List /* of BooleanFormula */ andorFormulas = new ArrayList();
	
	        for (int i=0; i<boolSwitchValues.length; i++) {
	        _countBoolNode();
	        BooleanFormula formulaInstance =
	            BooleanFormula.makeSwitch(boolSwitch, boolSwitchValues[i], result);
	        formulaInstance.setDescr(varName);
	        andorFormulas.add(formulaInstance);
	        }
	        _countBoolNode();
	        result = quant.equals(Quantifier.ALL) ?
	                	BooleanFormula.makeAnd(andorFormulas) :
	                    BooleanFormula.makeOr(andorFormulas);
	    }  // loop over quantified variables declared here
	    
	    return _saveTransl(quantForm_, new FormulaTransl(result));
    }  // visit(QuantifiedFormula ...)

    /**
	 * Translate a {@link ComprehensionExpr}to an {@link ExprTransl}. For each
	 * bit of the {@link ExprTransl}, we construct a {@link BooleanFormula}
	 * which sets the {@link BoolSwitch}es of the quantified variables in this
	 * comprehension to values corresponding to the coordinates of the bit.
	 */
    public Object visit(ComprehensionExpr compExpr_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(compExpr_));
	
	    int numQuantVars = 0;
	    for (DeclIter declIter = new DeclIter(compExpr_); declIter.hasNext();) {
	        declIter.next();
	        numQuantVars++;
	    }
	
	    QVarIterationInfo[] iterInfos = new QVarIterationInfo[numQuantVars];
	    int[] varRangeSizes = new int[numQuantVars];
	    LeafId[] varLeafIds = new LeafId[numQuantVars];
	    {
	        int varNum = 0;
	        for (DeclIter declIter = new DeclIter(compExpr_); declIter.hasNext();) {
	        declIter.next();
	        LeafId leafId = declIter.getLeafId();
	        varLeafIds[varNum] = leafId;
	        iterInfos[varNum] =
	            QVarValGenerator.constructQVarIterationInfo(leafId, _astInfoVisitor);
	        varRangeSizes[varNum] = iterInfos[varNum].getBoolSwitchValues().length;
	        _qvarIterInfo.put(leafId, iterInfos[varNum]);
	        varNum++;
	        }
	    }
	
	    FormulaTransl formulaTransl = (FormulaTransl)compExpr_.getFormula().applyReturnVisitor(this);
	    MultiDimArray result = _allocFormulas(compExpr_.getType().toRelationType());
	
	    int[] tupleIdx = new int[compExpr_.getType().toRelationType().numBasicTypes()];
	    for (MultiDimIter tupleIter = new MultiDimIter(varRangeSizes); tupleIter.hasNext();) {
	        int[] varSettings = (int[])tupleIter.next();
	        int dimStart = 0;
	        for (int i=0; i<varSettings.length; i++) {
	        int[] tupleCoords = iterInfos[i].getOneTupleCoords()[varSettings[i]];
	        System.arraycopy(tupleCoords, 0, tupleIdx, dimStart, tupleCoords.length);
	        dimStart += tupleCoords.length;
	        }
	
	        BooleanFormula bit = formulaTransl.formula;
	        for (int i=varSettings.length-1; i>=0; i--) {
	        bit =
	            BooleanFormula.makeSwitch(iterInfos[i].getBoolSwitch(),
	                          iterInfos[i].getBoolSwitchValues()[varSettings[i]],
	                          bit);
	        result.put(tupleIdx, bit);
	        }
	    }
	    return _saveTransl(compExpr_, new ExprTransl(compExpr_.getType().toRelationType(), result));
    }  // visit(ComprehensionExpr)

    private static int _computeBitNumber (RelationType relType_, int[] inds_, int dimStart_) {
    int flatInd = 0;
    int dsize = 1;
    for (int i=dimStart_ + relType_.numBasicTypes()-1; i>=dimStart_; i--) {
        flatInd += (inds_[i] * dsize);
        dsize *= relType_.getBasicTypeAt(i - dimStart_).getScope();
    }
    return flatInd;
    }


    /*************/
    /*** Exprs ***/
    /*************/

    public Object visit(BinaryExpr binaryExpr_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(binaryExpr_));
	    ExprTransl leftTransl = (ExprTransl)binaryExpr_.getLeft().applyReturnVisitor(this);
	    ExprTransl rightTransl = (ExprTransl)binaryExpr_.getRight().applyReturnVisitor(this);
	    Transl result = null;
	    
	    BinaryExprOp op = binaryExpr_.getOp();
	    if (op.equals(BinaryExprOp.JOIN_DOT) ||
	            op.equals(BinaryExprOp.JOIN_DOUBLECOLON) ||
	            op.equals(BinaryExprOp.JOIN_SQBRACKETS)) {
	        result = leftTransl.dot(rightTransl, binaryExpr_.getType().toRelationType());
	//      System.out.println(binaryExpr_.getLeft().nodeString() + " dot " +
	//                 binaryExpr_.getRight().nodeString() + " equals " +
	//                 result);
	    } else if (op.equals(BinaryExprOp.UNION)) {
	        result = leftTransl.union(rightTransl);
	    } else if (op.equals(BinaryExprOp.DIFF)) {
	        result = leftTransl.difference(rightTransl);
	    } else if (op.equals(BinaryExprOp.INTERSECT)) {
	        result = leftTransl.intersection(rightTransl);
	    } else if (op.equals(BinaryExprOp.RELATION)) {
	        result = leftTransl.arrow(rightTransl, binaryExpr_.getType().toRelationType());
	    }
	    
	    return _saveTransl(binaryExpr_, result);
    }

    public Object visit(GenericConstExpr genConstExpr_) {
    RelationType relType = genConstExpr_.getType().toRelationType();
    MultiDimArray formulas = _allocFormulas(relType);
    boolean isNoneExpr = (genConstExpr_ instanceof EmptySetExpr);
    boolean isUnivExpr = (genConstExpr_ instanceof UniversalExpr);
    boolean isIdenExpr = (genConstExpr_ instanceof IdentityExpr);
    for (MultiDimIter indsIter = new MultiDimIter(formulas.getDims());
         indsIter.hasNext();) {
        int[] inds = (int[])indsIter.next();
        formulas.put(inds,
             isNoneExpr ? BooleanFormula.FALSE() :
             (isUnivExpr ? BooleanFormula.TRUE() :
              (isIdenExpr ? BooleanFormula.makeConst(inds[0] == inds[1]) :
               null)));
    }
    return _saveTransl(genConstExpr_, new ExprTransl(genConstExpr_.getType().toRelationType(), formulas));
    }

    public Object visit(UniversalExpr univExpr_) { return visit((GenericConstExpr)univExpr_); }
    public Object visit(EmptySetExpr emptyExpr_) { return visit((GenericConstExpr)emptyExpr_); }
    public Object visit(IdentityExpr idenExpr_) { return visit((GenericConstExpr)idenExpr_); }

    public Object visit(UnaryExpr unaryExpr_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(unaryExpr_));
	    ExprTransl exprTransl = (ExprTransl)unaryExpr_.getExpr().applyReturnVisitor(this);
	    ExprTransl result = null;
	    UnaryExprOp op = unaryExpr_.getOp();
	    if (op.equals(UnaryExprOp.TRANSPOSE)) result = exprTransl.transpose(unaryExpr_.getType().toRelationType());
	    else if (op.equals(UnaryExprOp.TRANS_CLOSURE)) result = exprTransl.transitiveClosure();
	    else if (op.equals(UnaryExprOp.REF_TRANS_CLOSURE)) result = exprTransl.reflexiveTransitiveClosure();
	    return _saveTransl(unaryExpr_, result);
    }

    public Object visit(IfThenElseExpr ifThenElseExpr_) {
        BooleanFormula.setDefaultNodeSrc(getNodeID(ifThenElseExpr_));
        FormulaTransl ifTransl = (FormulaTransl)ifThenElseExpr_.getIfFormula().applyReturnVisitor(this);
        ExprTransl thenTransl = (ExprTransl)ifThenElseExpr_.getThenExpr().applyReturnVisitor(this);
        ExprTransl elseTransl = (ExprTransl)ifThenElseExpr_.getElseExpr().applyReturnVisitor(this);
        ExprTransl result = ExprTransl.ifThenElse(ifTransl, thenTransl, elseTransl);
        return _saveTransl(ifThenElseExpr_, result);
    }

    /****************/
    /*** IntExprs ***/
    /****************/

    public Object visit(LiteralIntExpr literalIntExpr_) {
        return _saveTransl(literalIntExpr_, IntTransl.fromIntConst(literalIntExpr_.getVal()));
    }

    public Object visit(ElemIntFormula elemIntFormula_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(elemIntFormula_));
	    IntExpr leftExpr = elemIntFormula_.getLeft();
	    IntExpr rightExpr = elemIntFormula_.getRight();
	    IntTransl leftTransl = (IntTransl)leftExpr.applyReturnVisitor(this);
	    IntTransl rightTransl = (IntTransl)rightExpr.applyReturnVisitor(this);
	    
	    FormulaTransl result;
	    IntCompOp op = elemIntFormula_.getOp();
	    if      (op.equals(IntCompOp.INT_EQUALS))    result = leftTransl.eq(rightTransl);
	    else if (op.equals(IntCompOp.INT_NOTEQUALS)) result = leftTransl.eq(rightTransl).not();
	    else if (op.equals(IntCompOp.INT_LTE))       result = leftTransl.le(rightTransl);
	    else if (op.equals(IntCompOp.INT_GTE))       result = leftTransl.ge(rightTransl);
	    else if (op.equals(IntCompOp.INT_LT))        result = leftTransl.lt(rightTransl);
	    else /*if (op.equals(IntCompOp.INT_GT))*/    result = leftTransl.gt(rightTransl);
	    return _saveTransl(elemIntFormula_, result);
    }

    public Object visit(BinaryIntExpr intExpr_) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(intExpr_));
	    IntTransl leftTransl = (IntTransl)intExpr_.getLeft().applyReturnVisitor(this);
	    IntTransl rightTransl = (IntTransl)intExpr_.getRight().applyReturnVisitor(this);
	    
	    if (intExpr_.getOp().equals(IntExprOp.PLUS)) {
	        return _saveTransl(intExpr_, leftTransl.plus(rightTransl));
	    } else if (intExpr_.getOp().equals(IntExprOp.MINUS)) {
	        return _saveTransl(intExpr_, leftTransl.minus(rightTransl));
	    } else {
	        throw new TranslException("Only integer addition and subtraction implemented at this time.");
	    }
    }

    public Object visit(CardinalityExpr cardExpr_ ) {
	    BooleanFormula.setDefaultNodeSrc(getNodeID(cardExpr_));
	    ExprTransl exprTransl = (ExprTransl)cardExpr_.getExpr().applyReturnVisitor(this);
	    return _saveTransl(cardExpr_, IntTransl.fromExprTransl(exprTransl));
    }

    public Object visit(IfThenElseIntExpr ifThenElseIntExpr_) {
        BooleanFormula.setDefaultNodeSrc(getNodeID(ifThenElseIntExpr_));
        FormulaTransl ifTransl = (FormulaTransl)ifThenElseIntExpr_.getIfFormula().applyReturnVisitor(this);
        IntTransl thenTransl = (IntTransl)ifThenElseIntExpr_.getThenIntExpr().applyReturnVisitor(this);
        IntTransl elseTransl = (IntTransl)ifThenElseIntExpr_.getElseIntExpr().applyReturnVisitor(this);
        IntTransl result = IntTransl.ifThenElse(ifTransl, thenTransl, elseTransl);
        return _saveTransl(ifThenElseIntExpr_, result);
    }

    public Object visit(SumExpr sumExpr_) {

	RelationType childRelType = sumExpr_.getExpr().getType().toRelationType();
	Dbg.chk(childRelType.numBasicTypes() == 1 &&
		childRelType.getBasicTypeAt(0) == getIntType());
	BasicType intType = childRelType.getBasicTypeAt(0);
	ExprTransl childTransl = (ExprTransl)sumExpr_.getExpr().applyReturnVisitor(this);
	
	IntTransl[] intAtomTransls = new IntTransl[intType.getScope()];
	for (int intAtom=0; intAtom<intType.getScope(); intAtom++) {
	    IntTransl atomTransl = _relationAllocator.getIntAtomTransl(intAtom);
	    BooleanFormula[] intBits = new BooleanFormula[_relationAllocator.getIntWidth()];
	    BooleanFormula atomInSet = childTransl.getTupleFormula(intAtom);
	    for (int intBit = 0; intBit < intBits.length; intBit++)
		intBits[intBit] = atomTransl.getBits()[intBit].and(atomInSet);
	    intAtomTransls[intAtom] = new IntTransl(intBits);
	}
	return _saveTransl(sumExpr_, IntTransl.makeSum(intAtomTransls));
    }

    public Object visit(ExprCastIntExpr sumExpr_) {

	RelationType childRelType = sumExpr_.getExpr().getType().toRelationType();
	
	Dbg.chk(childRelType.numBasicTypes() == 1 &&
		childRelType.getBasicTypeAt(0) == getIntType());
	BasicType intType = childRelType.getBasicTypeAt(0);
	ExprTransl childTransl = (ExprTransl)sumExpr_.getExpr().applyReturnVisitor(this);
	
	IntTransl[] intAtomTransls = new IntTransl[intType.getScope()];
	for (int intAtom=0; intAtom<intType.getScope(); intAtom++) {
	    IntTransl atomTransl = _relationAllocator.getIntAtomTransl(intAtom);
	    BooleanFormula[] intBits = new BooleanFormula[_relationAllocator.getIntWidth()];
	    BooleanFormula atomInSet = childTransl.getTupleFormula(intAtom);
	    for (int intBit = 0; intBit < intBits.length; intBit++)
		intBits[intBit] = atomTransl.getBits()[intBit].and(atomInSet);
	    intAtomTransls[intAtom] = new IntTransl(intBits, true /* signed integer */ );
	}
	return _saveTransl(sumExpr_, IntTransl.makeSum(intAtomTransls));
    }

    // Code for returning summary information about the Formula.
    // Can be called after the visitor has translated the entire AST.

    /**
	 * Return a {@link Map}from {@link Node}to its {@link Transl}ation.
	 * Called after this visitor has already translated the AST and accumulated
	 * the map in {@link #_node2transl}.
	 */
    public Map getNodeTranslations() { return _node2transl; }

    /**
	 * @return the {@link Transl}ation of a {@link Node}, or null if the node
	 *         doesn't have a translation (e.g. an {@link Op}node).
	 */
    public Transl getNodeTransl(Node node_) { return (Transl)_node2transl.get(node_); }


    /**
	 * Return a {@link Map}from the {@link LeafId}of each quantified
	 * {@link Variable}to the {@link BoolSwitch}allocated to it. Used by the
	 * Alloy Evaluator: when displaying the AST with the value of each node, for
	 * quantified variables, we need to be able to get the value of the formula
	 * for each setting of the {@link BoolSwitch}.
	 */
    //public Map getVarSwitches() { return _var2switch; }

    /**
	 * @return the {@link BoolSwitch}allocated to the quantified
	 *         {@link Variable}with the given {@link LeafId}.
	 */
    //public BoolSwitch getVarSwitch(LeafId varLeafId_) { return (BoolSwitch)Dbg.chk(_var2switch.get(varLeafId_)); }

    /**
	 * @return {@link Map}from {@link ExprTransl}translation of each relation
	 *         to its {@link RelationType}. Used by
	 *         {@link alloy.symm.SymmetryBreaker}to construct a
	 *         symmetry-breaking predicate.
	 */
    public Map getRelationTransls() {
    Map comp2type = new TreeMap();
    for (Iterator compIter = _relations.entrySet().iterator(); compIter.hasNext();) {
        Map.Entry compEntry = (Map.Entry)compIter.next();
        LeafId leafId = (LeafId)Dbg.chk(compEntry.getKey());
        LeafExpr leafExpr = (LeafExpr)Dbg.chk(compEntry.getValue());
        RelationType relType = leafExpr.getType().toRelationType();
        ExprTransl transl = (ExprTransl)Dbg.chk(_leafTransl.get(leafId));
        comp2type.put(transl, relType);
    }
    return comp2type;
    }

    /**
	 * @return {@link Map}from {@link LeafId}of each relation to a
	 *         {@link LeafExpr}for that relation.
	 */
    public Map getRelationReps() { return _astInfoVisitor.getRelationReps(); }

    /**
	 * @return {@link Map}from each {@link LeafId}to its {@link Transl}ation.
	 *         This includes leaves that are relations (translated to arrays of
	 *         Boolean variables), as well as leaves that are quantified
	 *         variables (translated to arrays of switchable constants).
	 */
    public Map getLeafTransls() { return _leafTransl; }

    /** @return translation of the given {@link LeafId} */
    public Transl getLeafTransl(LeafId leafId_) { return (Transl)Dbg.chk(_leafTransl.get(leafId_)); }

    /** @return the {@link RelationType} of leaves with the given {@link LeafId}. */
    public RelationType getLeafType(LeafId leafId_) {
    return _astInfoVisitor.getLeafType(leafId_);
    }

    /**
	 * @return the {@link MultiplicityExpr multiplicity}of quantified variable
	 *         with the given {@link LeafId}
	 */
    public MultiplicityExpr getLeafMultiplicity(LeafId leafId_) {
    return _astInfoVisitor.getLeafMultiplicity(leafId_);
    }

    /** @return the {@link Variable} object with the given {@link LeafId} */
    public Variable getVariable(LeafId leafId_) {
    return _astInfoVisitor.getVariable(leafId_);
    }

    /**
	 * @return {@link Map}from {@link LeafExpr}corresponding to each relation
	 *         to its {@link ExprTransl}. Used in constructing
	 *         {@link alloy.api.SolutionData}implementations.
	 * 
	 * Note that there may be many LeafExpr's for a given relation in the AST --
	 * one for each mention of the relation. Here we arbitrarily pick one for
	 * each relation.
	 * 
	 * @see alloy.api.SolutionDataImpl
	 */
    public Map /* LeafExpr->ExprTransl */ getRelationExprsToTransls() {
        Map /* LeafExpr->ExprTransl */ expr2transl = new TreeMap();
    for (Iterator compIter = _relations.entrySet().iterator(); compIter.hasNext();) {
        Map.Entry compEntry = (Map.Entry)compIter.next();
        LeafId leafId = (LeafId)compEntry.getKey();
        LeafExpr leafExpr = (LeafExpr)compEntry.getValue();
        ExprTransl transl = (ExprTransl)_leafTransl.get(leafId);
        expr2transl.put(leafExpr, transl);
    }
    return expr2transl;
    }

    /**
	 * @return the {@link BoolVarAllocator}used to allocate boolean variables
	 *         during translation. After translation, it can be queried for some
	 *         useful information such as how many boolean variables were
	 *         allocated to relations referenced in the {@link Formula}.
	 */
    public BoolVarAllocator getBoolVarAllocator() { return _boolVarAllocator; }

    public RelationAllocator getRelationAllocator() { return _relationAllocator; }

    /**
	 * @return all {@link BasicType}s used in the formula. The list of basic
	 *         types used is gathered during translation; calling this method
	 *         after translation returns what was gathered.
	 */
    public Set getBasicTypes() {
    return _astInfoVisitor.getBasicTypes();
    }

    /**
	 * @return the {@link BasicType}object representing the special Int basic
	 *         type, or null if Int is not used in the model.
	 */
    public BasicType getIntType() { return _astInfoVisitor.getIntType(); }

    /**
	 * @return the {@link VarCreator}that defined the quantified variable with
	 *         this {@link LeafId}.
	 */
    public VarCreator getVarCreator(LeafId leafId_) {
    return _astInfoVisitor.getVarCreator(leafId_);
    }

    /** Record the formula that we translated -- called once after translation. */
    private void _setFormula(Formula formula_) { 
    	// eclipse says this variable is never read, so this is a dead store
    	//_formula = formula_; 
    }

    /** @return the {@link Formula} translated by this {@link TranslVisitor}. */
    public Formula getFormula() { return _astInfoVisitor.getFormula(); }

    /** Return the command we were analyzing */
    public FindCommand getCommand() { return _astInfoVisitor.getCommand(); }

    /** Test whether the given {@link LeafId} is for a quantified variable. */
    public boolean isQuantVar(LeafId leafId_) { return _astInfoVisitor.isQuantVar(leafId_); }

    /**
	 * @return the parent {@link Node}of the given {@link Node}, or
	 *         <code>null</code> if the node is root of the AST.
	 */
    public Node getParent(Node node_) { return _astInfoVisitor.getParent(node_); }

    /** @return <code>true</code> iff anc_ is an ancestor of node_ */
    public boolean isAncestor(Node anc_, Node node_) { return _astInfoVisitor.isAncestor(anc_, node_); }

    /**
     * @return a representative {@link Leaf} with the given {@link LeafId}.
     */
    public Leaf getLeafRep(LeafId leafId_) { return _astInfoVisitor.getLeafRep(leafId_); }

    /**
	 * Test whether a given leaf is a skolem constant.
	 */
    public boolean isSkolemConstant(LeafId leafId_) {
    return _astInfoVisitor.isSkolemConstant(leafId_);
    }

    /**
	 * @return {@link Set}of {@link LeafId}s of relations.
	 * @see RelationAllocator
	 */
    public Set /* of LeafId */ getRelations() { return _astInfoVisitor.getRelations(); }

    /**
	 * Return a {@link QVarIterationInfo}object that describes the values
	 * through which the given quantified variable runs.
	 */
    public QVarIterationInfo getQVarIterationInfo(LeafId qvarLeafId_) {
    return (QVarIterationInfo)Dbg.chk(_qvarIterInfo.get(qvarLeafId_));
    }

    /**
	 * Return the {@link List}of {@link LeafId}s of quantified variables
	 * declared at the given given {@link Node}, in order of declaration. The
	 * list is empty unless the node is a {@link VarCreator}.
	 */
    public List /* of LeafId */ getVarsDeclaredAt(Node node_) {
    return _astInfoVisitor.getVarsDeclaredAt(node_);
    }

    /** Return an integer indicating the deterministic ID number of the given AST node */
    public int getNodeID(Node node_) { return _astInfoVisitor.getNodeID(node_); }

    public ASTInfoVisitor getASTInfoVisitor() { return _astInfoVisitor; }
}
